/*
 * Literal.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef LITERAL_HPP_
#define LITERAL_HPP_

#include <string>
#include <iostream>
#include <functional>

namespace bfr {

/**
 * A Literal is a propositional variable in positive or negative polarity.
 *
 * Literals are represented by a <i>variable id</i> and the polarity
 * of the occurrence. This is just a <code>bool</code> that is
 * <code>true</code> if the occurrence is positive and <code>false</code>
 * otherwise.
 */
class Literal {
    public:
        // static declarations
        /**
         * Symbol that is used to indicate that the occurrence is negative.
         */
        static const char NEG_SYMBOL = '~';

        /**
         * Constructor.
         *
         * @param id The id of this variable (each variable has an unique ID).
         * @param polarity The polarity of the the Literal.
         */
        explicit Literal(const size_t id, const bool polarity=true);

        /**
         * Copy constructor.
         *
         * @param other The other Literal to create a copy from.
         */
        explicit Literal(const Literal &other);

        /**
         * Destructor.
         */
        virtual ~Literal();

        /**
         * Returns the variable id.
         *
         * @return variable id.
         */
        inline size_t getId() const;

        /**
         * Return the polarity.
         * <br>
         * The polarity is <code>true</code> if the occurrence
         * is positive and <code>false</code> otherwise.
         *
         * @return polarity.
         */
        inline bool getPolarity() const;

        /**
         * Return the string representation of the variable.
         *
         * @return A string representing the variable of the Literal.
         */
        std::string variableString() const;

        /**
         * Write the string representation of the variable to the stream
         *
         * @param out The stream to write the string.
         *
         * @see variableString()
         */
        inline void variableString(std::ostream &out) const;

        /**
         * Get a human readable form of the Literal.
         *
         * @return variableString() or ~variableString, depending on the
         * polarity.
         */
        std::string asString() const;

        /**
         * Compare two Literals.
         *
         * @param other The Literal to compare this to.
         *
         * @return <code>true</code> if they have the same
         * variable id and polarity.
         */
        inline bool operator==(const Literal &other) const;

        /**
         * Return the hash value of this literal.
         *
         * It creates the hash value with boost::hash_combine.
         *
         * @return hash value.
         */
        size_t hashValue() const;

        /**
         * Write the Literal in a stream.
         *
         * @return The stream.
         */
        friend std::ostream& operator<<(std::ostream& os, const Literal &l);

        /**
         * Function to use in hash maps etc.
         */
        friend size_t hash_value(const Literal &literal);

    private:

        /**
         * Private default constructor, sets id to -1 (i. e. biggest possible
         * <code>size_t</code> value).
         */
        Literal();

        /**
         * Id of the variable.
         */
        size_t id;

        /**
         * Polarity of the variable.
         */
        bool polarity;
};

/**
 * @brief Struct that defines an operator() that accepts a Literal* and
 * returns its hash value, useful for hash maps etc.
 */
struct literal_hash_struct : public std::unary_function<const Literal&, size_t> {
    size_t operator() (const Literal &l) const {
        return l.hashValue();
    }
};

/**
 * @brief Struct that defines an operator() that accepts two Literal* and
 * performs an equality check, useful for hash maps etc.
 */
struct literal_equals_struct : public std::binary_function<const Literal&,
                                                            const Literal&,
                                                            bool> {
    bool operator() (const Literal &first,
                     const Literal &second) const {
        return first == second;
    }
};

// some inline methods

size_t Literal::getId() const {
    return id;
}

bool Literal::getPolarity() const {
    return polarity;
}

void Literal::variableString(std::ostream &out) const {
    out << 'x' << id;
}

bool Literal::operator ==(const Literal &other) const {
    return (id == other.id) && (polarity == other.polarity);
}

} // namespace bfr

#endif  // LITERAL_HPP_
